A:Type, eq:EqDecider(A), f:a:A fp Top, g:Top, x:A.
f  g(x) ~ if x  dom(f) f(x) else g(x) fi 

latex

Definitions	a:A fp B(a), x. t(x), Top, EqDecider(T), f  g, f(x)?z, f(x), Unit, P  Q, P & Q, P  Q, x  dom(f), , Prop, b, A, t  T, b, x:A. B(x)
Lemmas	assert wf, not wf, bnot wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, top wf, fpf wf